Iof proof for Lemma mul bounds 1a:
a, b:
. 0 
(a * b)
by ((UnivCD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))
C1:
C1: 1. a :
C1: 2. b :
C1: 0 (a * b)
C.| 12,41 |
a, b:. 0 (a * b)
by ((UnivCD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))
C1:
C1: 1. a :
C1: 2. b :
C1: 0 (a * b)
C.
| Definitions |  Tx:A. B(x) |
| Lemmas |